(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.
Start state: 3782
Accept states: [3783, 3784]
Transitions:
3782→3783[0_1|0]
3782→3784[5_1|0]
3782→3782[1_1|0, 2_1|0, 3_1|0, 4_1|0]
3782→3785[1_1|1]
3782→3788[1_1|1]
3782→3791[4_1|1]
3782→3795[1_1|1]
3782→3799[4_1|1]
3782→3804[2_1|1]
3782→3809[0_1|1]
3782→3814[4_1|1]
3782→3819[0_1|1]
3782→3824[0_1|1]
3782→3828[2_1|1]
3782→3833[2_1|1]
3785→3786[1_1|1]
3786→3787[2_1|1]
3787→3783[0_1|1]
3787→3809[0_1|1]
3787→3819[0_1|1]
3787→3824[0_1|1]
3788→3789[1_1|1]
3789→3790[3_1|1]
3790→3783[0_1|1]
3790→3809[0_1|1]
3790→3819[0_1|1]
3790→3824[0_1|1]
3791→3792[0_1|1]
3792→3793[3_1|1]
3793→3794[1_1|1]
3794→3783[1_1|1]
3794→3809[1_1|1]
3794→3819[1_1|1]
3794→3824[1_1|1]
3795→3796[2_1|1]
3796→3797[0_1|1]
3797→3798[2_1|1]
3798→3783[1_1|1]
3798→3809[1_1|1]
3798→3819[1_1|1]
3798→3824[1_1|1]
3799→3800[2_1|1]
3800→3801[1_1|1]
3801→3802[3_1|1]
3802→3803[0_1|1]
3803→3783[1_1|1]
3803→3809[1_1|1]
3803→3819[1_1|1]
3803→3824[1_1|1]
3804→3805[1_1|1]
3805→3806[2_1|1]
3806→3807[4_1|1]
3807→3808[0_1|1]
3808→3783[1_1|1]
3808→3809[1_1|1]
3808→3819[1_1|1]
3808→3824[1_1|1]
3809→3810[3_1|1]
3810→3811[4_1|1]
3811→3812[2_1|1]
3812→3813[1_1|1]
3813→3783[1_1|1]
3813→3809[1_1|1]
3813→3819[1_1|1]
3813→3824[1_1|1]
3814→3815[4_1|1]
3815→3816[0_1|1]
3816→3817[1_1|1]
3817→3818[2_1|1]
3818→3783[1_1|1]
3818→3809[1_1|1]
3818→3819[1_1|1]
3818→3824[1_1|1]
3819→3820[3_1|1]
3820→3821[1_1|1]
3821→3822[2_1|1]
3822→3823[2_1|1]
3823→3783[1_1|1]
3823→3809[1_1|1]
3823→3819[1_1|1]
3823→3824[1_1|1]
3824→3825[1_1|1]
3825→3826[3_1|1]
3826→3827[1_1|1]
3827→3783[1_1|1]
3827→3809[1_1|1]
3827→3819[1_1|1]
3827→3824[1_1|1]
3828→3829[1_1|1]
3829→3830[2_1|1]
3830→3831[1_1|1]
3831→3832[4_1|1]
3832→3784[5_1|1]
3833→3834[5_1|1]
3834→3835[3_1|1]
3835→3836[2_1|1]
3836→3784[1_1|1]